contradiction:=for_all(bool,(b:bool)b):bool.
by_contradiction(b:bool;p:proof(contradiction)):=
 specialize(bool,(b:bool)b,b,p):proof(b).

not(b:bool):=for_all(proof(b),(p:proof(b))contradiction):bool.
impossible(b:bool;p:proof(b);q:proof(not(b))):=
 specialize(proof(b),(p:proof(b))contradiction,p,q):proof(contradiction).
hence_not(b:bool;p:(q:proof(b))proof(contradiction)):=
 generalize(proof(b),(q:proof(b))contradiction,p):proof(not(b)).

modus_tollens(a,b:bool;p:proof(implies(a,b));q:proof(not(b))):=
 hence_not(a,(r:proof(a))impossible(b,modus_ponens(a,b,p,r),q)):proof(not(a)).

double_not(b:bool;p:proof(b)):=
 hence_not(not(b),(q:proof(not(b)))impossible(b,p,q)):proof(not(not(b))).

negation(t:atom;p:(x:t)bool):=(x:t)not(p(x)):(x:t)bool.
weakly_exists(t:atom;p:(x:t)bool):=not(for_all(t,negation(t,p))):bool.

step1(t:atom;p:(x:t)bool;q:proof(exists(t,p));r:proof(for_all(t,negation(t,p)))):=
 specialize(t,negation(t,p),choose(t,p,q),r):proof(not(p(choose(t,p,q)))).
step2(t:atom;p:(x:t)bool;q:proof(exists(t,p));r:proof(for_all(t,negation(t,p)))):=
 impossible(p(choose(t,p,q)),thus(t,p,q),step1(t,p,q,r)):proof(contradiction).
step3(t:atom;p:(x:t)bool;q:proof(exists(t,p))):=
 hence_not(for_all(t,negation(t,p)),step2(t,p,q)):proof(weakly_exists(t,p)).
fact1(t:atom;p:(x:t)bool):=
 implication(exists(t,p),weakly_exists(t,p),step3(t,p)):
 proof(implies(exists(t,p),weakly_exists(t,p))).

nonconstructive(t:atom;p:(x:t)bool):=#:
 proof(implies(weakly_exists(t,p),exists(t,p))).

trivial(b:bool):=proof(implies(b,b)):atom.
prop1(b:bool):=(p:trivial(b))b:(p:trivial(b))bool.
prop2(b:bool):=(p:trivial(b))not(b):(p:trivial(b))bool.
trick(b:bool):=for_all(trivial(b),prop2(b)):bool.
step1(b:bool;q:proof(trick(b))):=
 specialize(trivial(b),prop2(b),imp_refl(b),q):proof(not(b)).
step2(b:bool;p:proof(not(not(b)));q:proof(trick(b))):=
 impossible(not(b),step1(b,q),p):proof(contradiction).
step3(b:bool;p:proof(not(not(b)))):=
 hence_not(trick(b),step2(b,p)):proof(weakly_exists(trivial(b),prop1(b))).
step4(b:bool;p:proof(not(not(b)))):=
 modus_ponens(weakly_exists(trivial(b),prop1(b)),exists(trivial(b),prop1(b)),
  nonconstructive(trivial(b),prop1(b)),step3(b,p)):
 proof(exists(trivial(b),prop1(b))).
excluded_middle(b:bool;p:proof(not(not(b)))):=
 thus(trivial(b),prop1(b),step4(b,p)):proof(b).